A:Type, eq:EqDecider(A), f,g:fpf(A; a.top), x:A.
sqequal(fpf-dom(eq; x; fpf-join(eq; f; g)); bor(fpf-dom(eq; x; f); fpf-dom(eq; x; g))) 

latex

Definitions	t  T, x:A. B(x), b, guard(T), P  Q, top, P  Q, P  Q, x. t(x), P  Q, P  Q, fpf-join(eq; f; g), ff, , tt, A, b, prop{i:l}, Unit, EqDecider(T), fpf(A; a.B(a)), bor(p; q), sq_type(T), fpf-dom(eq; x; f), False
Lemmas	not functionality wrt iff, bool sq, fpf wf, deq wf, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool wf, eqtt to assert, fpf-join wf, fpf-join-dom, top wf, assert wf, fpf-dom wf